i:Id, k:Knd, l:IdLnk, ds:x:Id fp Type, da:a:Knd fp Type,
f:(tg:Id(State(ds)Valtype(da;k)(da(rcv(l,tg))?Void List))) List.
source(l) = i
 @i: with declarations 
 ds:ds
 da:da
 dk(v) sends f s v on link l 
 realizes es.
 (x:Id. vartype(i;x)  ds(x)?Top)
 & (e:E. loc(e) = i  Id  valtype(e)  Valtype(da;kind(e)))
 & (e:E. isrcv(e)  lnk(e) = l  IdLnk  valtype(e)  Valtype(da;kind(e)))
 & {m:Msg| source(mlnk(m)) = i }  Msg(l,tg. da(rcv(l,tg))?Top)
 & (e:E.
 & (loc(e) = i  Id
 & ( kind(e) = k  Knd
 & ( sends(l;e)
 & ( =
 & ( tagged-messages(l;z.z when e;val(e);f)
 & (  Msg(l,tg. da(rcv(l,tg))?Top) List) 

latex

Definitions

x:A. B(x), P  Q, Prop, t  T, x. t(x), A & B, P & Q, S  T, tagged-messages(l;s;v;L), State(ds), D realizes2 es.P(es), vartype(i;x), E, loc(e), valtype(e), kind(e), isrcv(e), lnk(e), sends(l;e), x when e, val(e), ES(the_w), es-T(es), 1of(t), 2of(t), es_info(es), rcvtype(e), acttype(e), es-eq(es), es-pred?(es), es_val(es), es-oaxioms(es), (state when e), es-M(es), tag(e), es-V(es), act(e), es_init(es), es-Trans(es), {T}, x(s), es is an event system of D, x:A. B(x), (Msg on l), haslink(l;m), f(x)?z, @i: with declarations ds:dsda:da k(v) sends f s v on link l, PossibleWorld(D;w), M.ds(x), M(i), M.init(x,v), M.pre(a,s,v), M.ef(k,x,s,v,w), M.send(k;l;s;v;ms;i), M.frame(k affects x), M.sframe(k sends <l,tg>), M.aframe(k affects x), M.bframe(k sends on l), with declarations ds:dsda:dak(v) sends f s v on link l, z != f(x)  P(a;z), x  dom(f), mk-ma, x : v, f(x), if b t else f fi, deq-member(eq;x;L), M.da(a), true, reduce(f;k;as), Y, a declared in M, unsolvable M.pre(a,s), msg(l;t;v), state_when(e), state_when(e)

Lemmas

d-realizes2-implies-realizes, d-single-sends wf, Id wf, lsrc wf, ma-state wf, ma-valtype wf, fpf-cap wf, Knd wf, Kind-deq wf, rcv wf, fpf wf, IdLnk wf, es-vartype wf, id-deq wf, top wf, es-E wf, es-loc wf, es-valtype wf, es-kind wf, assert wf, es-isrcv wf, es-lnk wf, es-Msg wf, mlnk wf2, Msg wf, es-sends wf, es-Msgl wf, map wf, tagged-list-messages wf, msg wf, fpf-cap-void-subtype, es-when wf, es-val wf, possible-world wf, fair-fifo wf, world wf, eqof eq btrue, loc wf, w-E wf, w-info wf